Inhalt des Dokuments
Publikationen
| Zitatschlüssel | bisping2016mechanical |
|---|---|
| Autor | Bisping, Benjamin and Brodmann, Paul-David and Jungnickel, Tim and Rickmann, Christina and Seidler, Henning and Stüber, Anke and Wilhelm-Weidner, Arno and Peters, Kirstin and Nestmann, Uwe |
| Buchtitel | International Conference on Interactive Theorem Proving |
| Seiten | 107–122 |
| Jahr | 2016 |
| DOI | 10.1007/978-3-319-43144-4_7 |
| Ort | Nancy, France |
| Jahrgang | 9807 |
| Monat | 8 |
| Verlag | Springer |
| Serie | Lecture Notes in Computer Science |
| Organisation | Springer International Publishing |
| Zusammenfassung | The impossibility of distributed consensus with one faulty process is a result with important consequences for real world distributed systems e.g., commits in replicated databases. Since proofs are not immune to faults and even plausible proofs with a profound formalism can conclude wrong results, we validate the fundamental result named FLP after Fischer, Lynch and Paterson by using the interactive theorem prover Isabelle/HOL. We present a formalization of distributed systems and the aforementioned consensus problem. Our proof is based on Hagen Völzer’s paper A constructive proof for FLP. In addition to the enhanced confidence in the validity of Völzer’s proof, we contribute the missing gaps to show the correctness in Isabelle/HOL. We clarify the proof details and even prove fairness of the infinite execution that contradicts consensus. Our Isabelle formalization may serve as a starting point for similar proofs of properties of distributed systems. |
Zusatzinformationen / Extras
Direktzugang
Schnellnavigation zur Seite über Nummerneingabe